Nuprl Definition : linorder 13,42
compound
Linorder(T;x,y.R(x;y)) == Order(T;x,y.R(x;y)) & Connex(T;x,y.R(x;y)) 
latex

Uprel 1, rel 1
Wellformedness Lemmaslinorder wf, linorder wf
DefinitionsP & Q, Order(T;x,y.R(x;y)), Connex(T;x,y.R(x;y))
FDL editor aliaseslinorder

origin